(set-logic QF_AX)
(set-info :status unsat)
(declare-sort I 0)
(declare-sort E 0)
(declare-fun a () (Array I E))
(declare-fun v () E)
(declare-fun i1 () I)
(declare-fun i2 () I)
(declare-fun i3 () I)
(declare-fun x () Bool)
(assert (=> x (= i2 i3)))
(assert (=> (not x) (= i2 i3)))
(assert (not (= i1 i2)))
(assert (not (= (select a i1) (select (store (store a i2 v) i3 v) i1))))
(check-sat)
